package edu.gatech.cc.concolic;

import edu.gatech.cc.concolic.constraint.Constraint;
import edu.gatech.cc.concolic.constraint.EQ;
import edu.gatech.cc.concolic.constraint.GE;
import edu.gatech.cc.concolic.constraint.GT;
import edu.gatech.cc.concolic.constraint.LE;
import edu.gatech.cc.concolic.constraint.LT;
import edu.gatech.cc.concolic.constraint.NE;
import edu.gatech.cc.concolic.expression.IntegerConstant;
import edu.gatech.cc.concolic.expression.IntegerExpression;
import edu.gatech.cc.concolic.expression.IntegerVariable;
import edu.gatech.cc.concolic.expression.LongConstant;
import edu.gatech.cc.concolic.expression.LongExpression;
import edu.gatech.cc.concolic.expression.SymbolicExpression;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.DynamicArea;
import gov.nasa.jpf.jvm.StackFrame;
import gov.nasa.jpf.jvm.bytecode.BALOAD;
import gov.nasa.jpf.jvm.bytecode.CALOAD;
import gov.nasa.jpf.jvm.bytecode.I2B;
import gov.nasa.jpf.jvm.bytecode.I2C;
import gov.nasa.jpf.jvm.bytecode.I2D;
import gov.nasa.jpf.jvm.bytecode.I2F;
import gov.nasa.jpf.jvm.bytecode.I2L;
import gov.nasa.jpf.jvm.bytecode.IADD;
import gov.nasa.jpf.jvm.bytecode.IALOAD;
import gov.nasa.jpf.jvm.bytecode.IAND;
import gov.nasa.jpf.jvm.bytecode.IDIV;
import gov.nasa.jpf.jvm.bytecode.IFEQ;
import gov.nasa.jpf.jvm.bytecode.IFGE;
import gov.nasa.jpf.jvm.bytecode.IFGT;
import gov.nasa.jpf.jvm.bytecode.IFLE;
import gov.nasa.jpf.jvm.bytecode.IFLT;
import gov.nasa.jpf.jvm.bytecode.IFNE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPGE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPGT;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPLE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPLT;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPNE;
import gov.nasa.jpf.jvm.bytecode.IINC;
import gov.nasa.jpf.jvm.bytecode.IMUL;
import gov.nasa.jpf.jvm.bytecode.INEG;
import gov.nasa.jpf.jvm.bytecode.IOR;
import gov.nasa.jpf.jvm.bytecode.IREM;
import gov.nasa.jpf.jvm.bytecode.ISHL;
import gov.nasa.jpf.jvm.bytecode.ISHR;
import gov.nasa.jpf.jvm.bytecode.ISUB;
import gov.nasa.jpf.jvm.bytecode.IUSHR;
import gov.nasa.jpf.jvm.bytecode.IXOR;
import gov.nasa.jpf.jvm.bytecode.L2D;
import gov.nasa.jpf.jvm.bytecode.L2F;
import gov.nasa.jpf.jvm.bytecode.L2I;
import gov.nasa.jpf.jvm.bytecode.LADD;
import gov.nasa.jpf.jvm.bytecode.LALOAD;
import gov.nasa.jpf.jvm.bytecode.LAND;
import gov.nasa.jpf.jvm.bytecode.LCMP;
import gov.nasa.jpf.jvm.bytecode.LDIV;
import gov.nasa.jpf.jvm.bytecode.LMUL;
import gov.nasa.jpf.jvm.bytecode.LNEG;
import gov.nasa.jpf.jvm.bytecode.LOOKUPSWITCH;
import gov.nasa.jpf.jvm.bytecode.LOR;
import gov.nasa.jpf.jvm.bytecode.LREM;
import gov.nasa.jpf.jvm.bytecode.LSHL;
import gov.nasa.jpf.jvm.bytecode.LSHR;
import gov.nasa.jpf.jvm.bytecode.LSUB;
import gov.nasa.jpf.jvm.bytecode.LUSHR;
import gov.nasa.jpf.jvm.bytecode.LXOR;
import gov.nasa.jpf.jvm.bytecode.TABLESWITCH;

public class DefaultExecutionStrategy implements ExecutionStrategy {

	private static String CONFIG_GENERATOR_NAME = "concolic.generator";

	private long intCnt;
	private long charCnt;

	public ProblemGenerator generator;
	
	public DefaultExecutionStrategy(Config config) {
		System.out.println("Concolic Execution Engine");

		intCnt = 0;
		charCnt = 0;

		try {
			generator = config.getInstance(CONFIG_GENERATOR_NAME, ProblemGenerator.class);
		}
		catch (Exception e) {
		}

		if (null == generator) {
			generator = new YicesBitVectorGenerator(config);
		}
			
	}

	public SymbolicExpression execute(IADD insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IADD(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(ISUB insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.ISUB(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(IMUL insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IMUL(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(IDIV insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IDIV(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(IREM insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IREM(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(IINC insn, StackFrame sf, int index, int increment) {
		IntegerExpression v1_s = (IntegerExpression) sf.getLocalAttr(index);

		if (v1_s != null) {
			return new edu.gatech.cc.concolic.expression.IINC(v1_s, increment);
		}

		return null;
	}

	public SymbolicExpression execute(INEG insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			return new edu.gatech.cc.concolic.expression.INEG(v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(IAND insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IAND(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(IOR insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IOR(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(IXOR insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			return new edu.gatech.cc.concolic.expression.IXOR(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(ISHL insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr(0);
		int amount = sf.peek(0);
		IntegerExpression expr_s = (IntegerExpression) sf.getOperandAttr(1);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.ISHL(expr_s, amount_s);
		}

		return null;
	}

	public SymbolicExpression execute(ISHR insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr(0);
		int amount = sf.peek(0);
		IntegerExpression expr_s = (IntegerExpression) sf.getOperandAttr(1);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.ISHL(expr_s, amount_s);
		}

		return null;
	}

	public SymbolicExpression execute(IUSHR insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr(0);
		int amount = sf.peek(0);
		IntegerExpression expr_s = (IntegerExpression) sf.getOperandAttr(1);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.ISHL(expr_s, amount_s);
		}

		return null;
	}

	public SymbolicExpression execute(I2B insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		return v1_s;
	}

	public SymbolicExpression execute(I2C insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		return v1_s;
	}

	public SymbolicExpression execute(I2D insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			throw new UnsupportedOperationException("## Error: " + insn.getClass().getSimpleName() + " at "
					+ sf.getMethodName() + ":" + sf.getLine());
		}

		return null;
	}

	public SymbolicExpression execute(I2F insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			throw new UnsupportedOperationException("## Error: " + insn.getClass().getSimpleName() + " at "
					+ sf.getMethodName() + ":" + sf.getLine());
		}

		return null;
	}

	public SymbolicExpression execute(I2L insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			return new edu.gatech.cc.concolic.expression.I2L(v1_s);
		}

		return v1_s;

	}

	public SymbolicExpression execute(L2D insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			throw new UnsupportedOperationException("## Error: " + insn.getClass().getSimpleName() + " at "
					+ sf.getMethodName() + ":" + sf.getLine());
		}

		return null;
	}

	public SymbolicExpression execute(L2F insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			throw new UnsupportedOperationException("## Error: " + insn.getClass().getSimpleName() + " at "
					+ sf.getMethodName() + ":" + sf.getLine());
		}

		return null;
	}

	public SymbolicExpression execute(L2I insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			return new edu.gatech.cc.concolic.expression.L2I(v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LADD insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LADD(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(LAND insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LAND(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(LCMP insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LCMP(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LDIV insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LDIV(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LMUL insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LMUL(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(LNEG insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);

		if (v1_s != null) {
			return new edu.gatech.cc.concolic.expression.LNEG(v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LOR insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LOR(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(LREM insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LREM(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LSUB insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LSUB(v2_s, v1_s);
		}

		return null;
	}

	public SymbolicExpression execute(LXOR insn, StackFrame sf) {
		LongExpression v1_s = (LongExpression) sf.getOperandAttr(1);
		long v1 = sf.longPeek(0);
		LongExpression v2_s = (LongExpression) sf.getOperandAttr(3);
		long v2 = sf.longPeek(2);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new LongConstant(v1);
			if (v2_s == null) v2_s = new LongConstant(v2);

			return new edu.gatech.cc.concolic.expression.LXOR(v1_s, v2_s);
		}

		return null;
	}

	public SymbolicExpression execute(LSHL insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr();
		int amount = sf.peek(0);
		LongExpression expr_s = (LongExpression) sf.getOperandAttr(2);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.LSHL(expr_s, amount_s);
		}

		return null;
	}

	public SymbolicExpression execute(LSHR insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr();
		int amount = sf.peek(0);
		LongExpression expr_s = (LongExpression) sf.getOperandAttr(2);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.LSHR(expr_s, amount_s);
		}

		return null;
	}

	public SymbolicExpression execute(LUSHR insn, StackFrame sf) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr();
		int amount = sf.peek(0);
		LongExpression expr_s = (LongExpression) sf.getOperandAttr(2);

		if (expr_s != null) {
			if (amount_s == null) amount_s = new IntegerConstant(amount);
			return new edu.gatech.cc.concolic.expression.LUSHR(expr_s, amount_s);
		}

		return null;
	}

	/******************************/

	public void execute(IF_ICMPEQ insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 == v1) ? new EQ(v2_s, v1_s) : new NE(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IF_ICMPNE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 != v1) ? new NE(v2_s, v1_s) : new EQ(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IF_ICMPGE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		System.out.println("IF_ICMPGE");
		
		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 >= v1) ? new GE(v2_s, v1_s) : new LT(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IF_ICMPGT insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 > v1) ? new GT(v2_s, v1_s) : new LE(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IF_ICMPLE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 <= v1) ? new LE(v2_s, v1_s) : new GT(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IF_ICMPLT insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		int v1 = sf.peek(0);
		IntegerExpression v2_s = (IntegerExpression) sf.getOperandAttr(1);
		int v2 = sf.peek(1);

		if (v1_s != null || v2_s != null) {
			if (v1_s == null) v1_s = new IntegerConstant(v1);
			if (v2_s == null) v2_s = new IntegerConstant(v2);

			Constraint c = (v2 < v1) ? new LT(v2_s, v1_s) : new GE(v2_s, v1_s);
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFEQ insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 == 0) ? new EQ(v1_s, new LongConstant(0)) : new NE(v1_s, new LongConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFNE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		
		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 != 0) ? new NE(v1_s, new LongConstant(0)) : new EQ(v1_s, new LongConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFGE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 >= 0) ? new GE(v1_s, new LongConstant(0)) : new LT(v1_s, new LongConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFGT insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 > 0) ? new GT(v1_s, new IntegerConstant(0)) : new LE(v1_s, new IntegerConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFLE insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		
		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 <= 0) ? new LE(v1_s, new IntegerConstant(0)) : new GT(v1_s, new IntegerConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IFLT insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);
		
		if (v1_s != null) {
			int v1 = sf.peek(0);
			Constraint c = (v1 < 0) ? new LT(v1_s, new IntegerConstant(0)) : new GE(v1_s, new IntegerConstant(0));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(LOOKUPSWITCH insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if(v1_s != null) {
			int value = sf.peek(0);
			Constraint c = new EQ(v1_s, new LongConstant(value));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(TABLESWITCH insn, StackFrame sf) {
		IntegerExpression v1_s = (IntegerExpression) sf.getOperandAttr(0);

		if(v1_s != null) {
			int value = sf.peek(0);
			Constraint c = new EQ(v1_s, new IntegerConstant(value));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(BALOAD insn, StackFrame sf, DynamicArea da) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr(0);
		
		if (amount_s != null) {
			int amount = sf.peek(0);
			Constraint c = new EQ(amount_s, new IntegerConstant(amount));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(CALOAD insn, StackFrame sf, DynamicArea da) {
		IntegerExpression index_s = (IntegerExpression) sf.getOperandAttr(0);

		if (index_s != null) {
			int index = sf.peek(0);
			Constraint c = new EQ(index_s, new IntegerConstant(index));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(IALOAD insn, StackFrame sf, DynamicArea da) {
		IntegerExpression index_s = (IntegerExpression) sf.getOperandAttr(0);

		if (index_s != null) {
			int amount = sf.peek(0);
			Constraint c = new EQ(index_s, new IntegerConstant(amount));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(LALOAD insn, StackFrame sf, DynamicArea da) {
		IntegerExpression amount_s = (IntegerExpression) sf.getOperandAttr(0);

		if (amount_s != null) {
			int amount = sf.peek(0);
			Constraint c = new EQ(amount_s, new IntegerConstant(amount));
			generator.addConstraint(c, insn.getSourceLocation());
		}
	}

	public void execute(Exception exception) {
		generator.close();
	}

	public void exit() {
		generator.close();
	}

	/******************************/

	public SymbolicExpression makeSymbolic(int x) {
		IntegerVariable var = new IntegerVariable("int" + intCnt++);
		generator.addVariable(var);
		return var;

	}

	public SymbolicExpression makeSymbolic(char c) {
		IntegerVariable var = new IntegerVariable("char" + charCnt++);
		generator.addVariable(var);
		return var;
	}		
}
